Termination of the following Term Rewriting System could be disproven:

Generalized rewrite system (where rules with free variables on rhs are allowed):
The TRS R consists of the following rules:

U11(tt) → snd(splitAt(N, XS))
U161(tt) → cons(N)
U171(tt) → head(afterNth(N, XS))
U181(tt) → Y
U191(tt) → pair(nil, XS)
U201(tt) → U202(splitAt(N, XS))
U202(pair(YS, ZS)) → pair(cons(X), ZS)
U21(tt) → X
U211(tt) → XS
U221(tt) → fst(splitAt(N, XS))
U31(tt) → N
and(tt) → X
U101(tt) → U102(isNatural)
U102(tt) → U103(isLNat)
U103(tt) → tt
U111(tt) → U112(isLNat)
U112(tt) → tt
U121(tt) → U122(isNatural)
U122(tt) → tt
U131(tt) → U132(isNatural)
U132(tt) → U133(isLNat)
U133(tt) → tt
U141(tt) → U142(isLNat)
U142(tt) → U143(isLNat)
U143(tt) → tt
U151(tt) → U152(isNatural)
U152(tt) → U153(isLNat)
U153(tt) → tt
U41(tt) → U42(isNatural)
U42(tt) → U43(isLNat)
U43(tt) → tt
U51(tt) → U52(isNatural)
U52(tt) → U53(isLNat)
U53(tt) → tt
U61(tt) → U62(isPLNat)
U62(tt) → tt
U71(tt) → U72(isNatural)
U72(tt) → tt
U81(tt) → U82(isPLNat)
U82(tt) → tt
U91(tt) → U92(isLNat)
U92(tt) → tt
afterNth(N, XS) → U11(and(and(isNatural)))
fst(pair(X, Y)) → U21(and(and(isLNat)))
head(cons(N)) → U31(and(and(isNatural)))
isLNattt
isLNatU41(and(isNaturalKind))
isLNatU51(and(isNaturalKind))
isLNatU61(isPLNatKind)
isLNatU71(isNaturalKind)
isLNatU81(isPLNatKind)
isLNatU91(isLNatKind)
isLNatU101(and(isNaturalKind))
isLNatKindtt
isLNatKindand(isNaturalKind)
isLNatKindisPLNatKind
isLNatKindisNaturalKind
isLNatKindisLNatKind
isNaturaltt
isNaturalU111(isLNatKind)
isNaturalU121(isNaturalKind)
isNaturalU131(and(isNaturalKind))
isNaturalKindtt
isNaturalKindisLNatKind
isNaturalKindisNaturalKind
isNaturalKindand(isNaturalKind)
isPLNatU141(and(isLNatKind))
isPLNatU151(and(isNaturalKind))
isPLNatKindand(isLNatKind)
isPLNatKindand(isNaturalKind)
natsFrom(N) → U161(and(isNatural))
sel(N, XS) → U171(and(and(isNatural)))
snd(pair(X, Y)) → U181(and(and(isLNat)))
splitAt(0, XS) → U191(and(isLNat))
splitAt(s(N), cons(X)) → U201(and(and(isNatural)))
tail(cons(N)) → U211(and(and(isNatural)))
take(N, XS) → U221(and(and(isNatural)))



GTRS
  ↳ CritRuleProof

Generalized rewrite system (where rules with free variables on rhs are allowed):
The TRS R consists of the following rules:

U11(tt) → snd(splitAt(N, XS))
U161(tt) → cons(N)
U171(tt) → head(afterNth(N, XS))
U181(tt) → Y
U191(tt) → pair(nil, XS)
U201(tt) → U202(splitAt(N, XS))
U202(pair(YS, ZS)) → pair(cons(X), ZS)
U21(tt) → X
U211(tt) → XS
U221(tt) → fst(splitAt(N, XS))
U31(tt) → N
and(tt) → X
U101(tt) → U102(isNatural)
U102(tt) → U103(isLNat)
U103(tt) → tt
U111(tt) → U112(isLNat)
U112(tt) → tt
U121(tt) → U122(isNatural)
U122(tt) → tt
U131(tt) → U132(isNatural)
U132(tt) → U133(isLNat)
U133(tt) → tt
U141(tt) → U142(isLNat)
U142(tt) → U143(isLNat)
U143(tt) → tt
U151(tt) → U152(isNatural)
U152(tt) → U153(isLNat)
U153(tt) → tt
U41(tt) → U42(isNatural)
U42(tt) → U43(isLNat)
U43(tt) → tt
U51(tt) → U52(isNatural)
U52(tt) → U53(isLNat)
U53(tt) → tt
U61(tt) → U62(isPLNat)
U62(tt) → tt
U71(tt) → U72(isNatural)
U72(tt) → tt
U81(tt) → U82(isPLNat)
U82(tt) → tt
U91(tt) → U92(isLNat)
U92(tt) → tt
afterNth(N, XS) → U11(and(and(isNatural)))
fst(pair(X, Y)) → U21(and(and(isLNat)))
head(cons(N)) → U31(and(and(isNatural)))
isLNattt
isLNatU41(and(isNaturalKind))
isLNatU51(and(isNaturalKind))
isLNatU61(isPLNatKind)
isLNatU71(isNaturalKind)
isLNatU81(isPLNatKind)
isLNatU91(isLNatKind)
isLNatU101(and(isNaturalKind))
isLNatKindtt
isLNatKindand(isNaturalKind)
isLNatKindisPLNatKind
isLNatKindisNaturalKind
isLNatKindisLNatKind
isNaturaltt
isNaturalU111(isLNatKind)
isNaturalU121(isNaturalKind)
isNaturalU131(and(isNaturalKind))
isNaturalKindtt
isNaturalKindisLNatKind
isNaturalKindisNaturalKind
isNaturalKindand(isNaturalKind)
isPLNatU141(and(isLNatKind))
isPLNatU151(and(isNaturalKind))
isPLNatKindand(isLNatKind)
isPLNatKindand(isNaturalKind)
natsFrom(N) → U161(and(isNatural))
sel(N, XS) → U171(and(and(isNatural)))
snd(pair(X, Y)) → U181(and(and(isLNat)))
splitAt(0, XS) → U191(and(isLNat))
splitAt(s(N), cons(X)) → U201(and(and(isNatural)))
tail(cons(N)) → U211(and(and(isNatural)))
take(N, XS) → U221(and(and(isNatural)))


The rule U11(tt) → snd(splitAt(N, XS)) contains free variables in its right-hand side. Hence the TRS is not-terminating.